$\vdash$  tt = tt